D1, D2, D3:Dsys. D1  D2  D2  D3  D1  D3 

latex

Definitions	Id, t  T, x:A. B(x), M1  M2, D1  D2, Dsys, P  Q, M(i)
Lemmas	ma-sub transitivity, d-m wf, d-sub wf, dsys wf, Id wf